\begin{nusmvCommand} {check\_ltlspec\_sbmc\_inc} {\label{checkLtlspecSBmcInc}
Checks the given LTL specification, or all LTL specifications if no
formula is given.  Checking parameters are the maximum length and the
loopback value}

\cmdLine{check\_ltlspec\_sbmc\_inc [-h | -n idx | -p "formula [IN context]"]
[-k max\_length] [-o filename] [-N] [-c]}

This command generates one or more problems, and calls SAT solver for
each one. The Incremental BMC encoding used is the one by of Heljanko,
Junttila and Latvala, as described in~\cite{cav05}.
%
For each problem this command incrementally generates many
satisfiability subproblems and calls the SAT solver on each one of
them.
%
Each problem is related to a specific problem bound, which
increases from zero ($0$) to the given maximum problem length. Here
\code{max\_length} is the bound of the problem that system is going to
generate and solve.  In this context the maximum problem bound is
represented by the \commandopt{k} command parameter, or by its default
value stored in the environment variable \envvar{bmc\_length}. 

The property to be checked may be specified using the \commandopt{n
idx} or the \commandopt{p "formula"} options.  If you need to generate
a DIMACS dump file of all generated problems, you must use the option
\command{-o "filename"}.

\begin{cmdOpt}

\opt{-n \parameter{\natnum{\it index}}}{\natnum{\it index} is the
numeric index of a valid LTL specification formula actually located in
the properties database.}
       
\opt{-p \parameter{"\anyexpr [IN context]"}}{Checks the \anyexpr specified on
the command-line. \code{context} is the module instance name which
the variables in \anyexpr must be evaluated in.}
            
\opt{-k \parameter{\natnum{\it max\_length}}}{\natnum{\it max\_length} is the maximum problem
bound to be checked. Only natural numbers are valid values for this
option. If no value is given the environment variable \envvar{\it
bmc\_length} is considered instead.}

\opt{-o \parameter{\filename{\it filename}}}{\filename{\it filename} is the name of the dumped
dimacs file.  It may contain special symbols which will be
macro-expanded to form the real file name. Possible symbols are: }
       \tabItem{@F: model name with path part. }
       \tabItem{@f: model name without path part.} 
       \tabItem{@k: current problem bound.} 
       \tabItem{@l: current loopback value.} 
       \tabItem{@n: index of the currently processed formula in the property 
       database.} 
       \tabItem{@@: the `@' character.}

\opt{-N} {Does not perform virtual unrolling.}

\opt{-c} {Performs completeness check.}

\end{cmdOpt}
\end{nusmvCommand}
